es:ES, i, x:Id, T, A:Type, f:(TA).
@i(x:T)  e@i. f((x after e)) = f(x when e)  e@i. f(x when e) = f(x when es-init(es;e)) 

latex

Definitions	T, True, if b then t else f fi , tt, b, x. t(x), t  T, A c B, , x(s), e@i. P(e), P  Q, x:A. B(x), @i always.P(x), P & Q, @i(x:T)
Lemmas	true wf, squash wf, es-first-init, es-first-unique, event system wf, es-dtype wf, es-after wf, alle-at wf, es-E wf, Id wf, es-loc wf, es-first wf, assert wf, es-vartype wf, es-loc-init, es-init wf, es-when wf, es-invariant1